Module isotope::prelude[][src]

Expand description

Commonly used items

Re-exports

pub use ctx::cons::ConsCtx;
pub use ctx::eq::Structural;
pub use ctx::eq::TermEqCtx;
pub use ctx::eq::TermEqCtxEdit;
pub use ctx::eq::TermEqCtxMut;
pub use ctx::eq::Typed;
pub use ctx::eq::Untyped;
pub use ctx::eval::Reduce;
pub use ctx::eval::ReductionConfig;
pub use ctx::subst::EvalCtx;
pub use ctx::subst::SubstCtx;
pub use ctx::ty::BinaryCtx;
pub use ctx::ty::Trivial;
pub use ctx::ty::TrivialCons;
pub use ctx::ty::TyCtxMut;
pub use ctx::ty::TRIVIAL;
pub use ctx::StandardCtx;
pub use program::NodeIx;
pub use term::dynamic::DynamicTerm;
pub use term::dynamic::DynamicValue;
pub use term::flags::AtomicTyckFlags;
pub use term::flags::TyckFlag;
pub use term::flags::TyckFlags;
pub use term::weak::WeakId;
pub use term::Cons;
pub use term::HasDependencies;
pub use term::Substitute;
pub use term::Term;
pub use term::TermEq;
pub use term::TermId;
pub use term::Typecheck;
pub use term::Value;

Structs

Annotation

An owned type annotation

App

A function application, with an optional type annotation

Case

A case expression, which switches on variants to return a value

DisjointSetCtx

A standard context for hash-consing and equality checking

Enum

A type with a finite number of named variants

Id

The identity type, representing proofs that two terms are equal

Lambda

A lambda function

NormalCfg

A reduction configuration to keep going until reaching a given form for up to n compound reductions.

Pi

A dependent function type

ReduceUntil

A reduction configuration to keep going until a given condition has been reached, delegating otherwise to another configuration

Refl

The reflexivity axiom: asserts that the left hand side and right hand side are judgementally equal, and therefore propositionally equal

Shift

Shift a term up or down by an amount

SubstSlice

A simple slice of substitutions

SubstVec

A simple vector of substitutions

Universe

A typing universe

UniverseTerm

A term containing a typing universe

Var

A variable, represented by a de-Bruijn index

VarFilter

A filter for variables

Variant

A variant of an enumeration

Enums

AnnotationRef

A borrowed type annotation

Form

Forms a term can be in

Traits

AnnotationLike

A term which behaves like a (potentially borrowed) annotation

OptionalValue

A convenience trait implemented by Option<V> where V is a value